$\forall$$S$,$T$:Type, $f$:($S$$\rightarrow$$T$), $b$:$\mathbb{B}$, $p$,$q$:$S$. $f$(if $b$ then $p$ else $q$ fi ) = if $b$ then $f$($p$) else $f$($q$) fi